(TML)

  %We now set up the remaining required identities as
   a list of formulae.
  %

["HEAD UU == UU"
;"HEAD NIL == UU"
;"HEAD (CONS A L) == A"
;"TAIL UU == UU"
;"TAIL NIL == UU"
;"TAIL (CONS A L) == L"
]
  ;;

map prove it
    where prove fm =
          let (),proof = SIMPTAC(fm,ss,[])
                 where ss = 
                       itlist ssadd [defHEAD;defTAIL;defNIL;defCONS]
                              BASICSS
           in proof[];;

let proof = it;;




let [HEADUUthm;HEADNILthm;HEADCONSthm;TAILUUthm;TAILNILthm;
     TAILCONSthm] = it;;